Simulation-based verification algorithms can provide formal safety guarantees for nonlinear and hybrid systems. Most models that are constructed by engineers in the process of designing systems are in fact nonlinear. The hybrid aspect arises when there is a switch from one nonlinear model to a different nonlinear model, owing to, for example, changes in the environment, user inputs, or failures.
For nonlinear dynamical systems that do not admit analytic solutions, one relies exclusively on numerical simulations. Though simulations give sufficient confidence for design, testing, and performance analysis in many application scenarios, for mathematical guarantees or verification, simulations are of limited use. Particularly resistant to simulation-based verification are nonlinear models with large sets of initial conditions, inputs, and unknown parameters.
Previous algorithms rely on user provided model annotations called discrepancy functions, which are used for computing reachtubes from simulations. A reachtube is a mathematical construct of over-approximations to capture all possible behaviors that can arise from inputs and initial states of a simulation of a physical system.